$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$${\it e'}$:E. Dec($P$(${\it e'}$)))
\\[0ex]$\Rightarrow$ ($\forall$$l$:IdLnk, $e$:E. Dec($\exists$${\it e'}$:E. (($\uparrow$isrcv(${\it e'}$)) \& lnk(${\it e'}$) = $l$ \& sender(${\it e'}$) = $e$ \& $P$(${\it e'}$))))